package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;

import ast.*;

public class TermJudgement extends FLJudgement {
	
	private Term t;
	private PsiNode psi;
	private ResNode res;
	
	public TermJudgement(Term trm, HashMap<String, HashSet<Term>> rho)
	{
		t = trm;
		setRho(rho);
		psi = new PsiNode();
		res = new ResNode();
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public ResNode getRes()
	{
		return res;
	}
	
	public String toString()
	{
		String res = "";
		res += getRho() + " |- " + t + " : " + psi + " & " + this.res;
		return res;
	}
	
	public ArrayList<DischargeResult> discharge()
	{
		ArrayList<DischargeResult> resList = new ArrayList<DischargeResult>();
		
		Set<String> dataConstantNames = STSimplifier.getDataMap().keySet();
		Set<String> channelConstantNames = STSimplifier.getChannelMap().keySet();
		Set<String> principalNames = STSimplifier.getPrincipals();
		
		
		if (t instanceof TermVar) {
			
			
			if (dataConstantNames.contains(((TermVar) t).getName())) {
			// the free occurrence of t is actually a constant
				
				HashSet<Term> constantSet = new HashSet<Term>();
				constantSet.add(ExternalData.getInstance());
				ResNode csn = new ResNode(constantSet);
				resList.add(new Inclusion(csn, res, true));
				
			} else if (channelConstantNames.contains(((TermVar) t).getName())) {
				
				HashSet<Term> constantSet = new HashSet<Term>();
				constantSet.add(
						STSimplifier.getChannelMap().get(((TermVar) t).getName()));
				ResNode dan = new ResNode(constantSet);
				resList.add(new Inclusion(dan, res, true));
				
			} else if (principalNames.contains(((TermVar) t).getName())) {
				
				HashSet<Term> constantSet = new HashSet<Term>();
				constantSet.add(new Principal(((TermVar) t).getName()));
				ResNode prn = new ResNode(constantSet);
				resList.add(new Inclusion(prn, res, true));
				
			} else { // the free occurrence of t is really a variable
				
				FreeVariable fv = new FreeVariable(((TermVar) t).getName());
				resList.add(new Inclusion(new RhoNode(fv), res, true));
				
			}
		
		} else if (t instanceof FunApp) {
			
			Function func = STSimplifier.getFunctionMap().get(
					((FunApp) t).getName());
			
			ArrayList<FreeVariable> fvs = new ArrayList<FreeVariable>();
			int arity = func.getSignature().getFst().size();
			for (int i = 0; i < arity; i++) {
				fvs.add(new FreeVariable("#v" + (i + 1)));
			}
			FunNode fn = new FunNode(func, fvs);
			
			assert arity > 0;
			HashSet<Node> singletonFun = new HashSet<Node>();
			singletonFun.add(fn);
			Inclusion incl = new Inclusion(new ConcreteSetNode(singletonFun), res, true);
			Constraint forallConstraint = incl;
			TermJudgement curJgt;
			for (int i = arity - 1; i >= 0; i--) {
				curJgt = new TermJudgement(((FunApp) t).getArgList().get(i), getRho());
				resList.add(curJgt);
				resList.add(new Inclusion(curJgt.getRes(), res, true));
				forallConstraint = new ForallConstraint(
						new BoundVariable(fvs.get(i).getName()),
						curJgt.getRes(),
						forallConstraint);
			}
			
			resList.add(forallConstraint);
			
		} else if (t instanceof Endorse) {
			
			TermJudgement tjgt = new TermJudgement(((Endorse) t).getT(), getRho());
			resList.add(tjgt);
			resList.add(new Inclusion(tjgt.getPsi(), psi, true));
			resList.add(new Inclusion(tjgt.getRes(), res, true));
			HashSet<Node> tpSet = new HashSet<Node>();
			tpSet.add(new TpNode(new FreeVariable("#v")));
			HashSet<Node> chSet = new HashSet<Node>();
			chSet.add(ChannelTp.getInstance());
			HashSet<Node> srtSet = new HashSet<Node>();
			srtSet.add(SrtSignal.getInstance());

		}
		
		return resList;
	}
	
}
